@TechReport{Subotic2010,
author = {Paul Subotic and Ramunas Gutkovas},
title = {Provably Correct Software Project: Behaviourly correct MIPS simulator},
institution = {Uppsala university},
year = {2010},
OPTmonth = {June}
}



@inproceedings{DBLP:conf/cgo/LattnerA04,
  author    = {Chris Lattner and
               Vikram S. Adve},
  title     = {LLVM: A Compilation Framework for Lifelong Program Analysis
               {\&} Transformation},
  booktitle = {CGO},
  year      = {2004},
  pages     = {75-88},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CGO.2004.1281665},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{Marc20113,
	title = {On {U}sing {B} in the {D}esign of {S}ecure {M}icro-controllers: {A}n {E}xperience {R}eport},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {280},
	number = {0},
	pages = {3 - 22},
	year = {2011},
	note = {Proceedings of the B 2011 Workshop, a satellite event of the 17th International Symposium on Formal Methods (FM 2011)},
	issn = {1571-0661},
	doi = {10.1016/j.entcs.2011.11.014},
	url = {http://www.sciencedirect.com/science/article/pii/S1571066111001630},
	author = {Marc Benveniste},
	keywords = {formal development flow},
	keywords = {digital circuit},
	keywords = {robustness},
	keywords = {secure micro-controller},
	keywords = {correct by construction}
}



@inproceedings{springerlink:Yuan2011,
  author    = {Fangfang Yuan and
               Stephen Wright and
               Kerstin Eder and
               David May},
  title     = {Managing Complexity through Abstraction: A Refinement-Based
               Approach to Formalize Instruction Set Architectures},
  booktitle = {ICFEM},
  year      = {2011},
  pages     = {585-600},
  ee        = {http://dx.doi.org/10.1007/978-3-642-24559-6_39},
  crossref  = {DBLP:conf/icfem/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icfem/2011,
  editor    = {Shengchao Qin and
               Zongyan Qiu},
  title     = {Formal Methods and Software Engineering - 13th International
               Conference on Formal Engineering Methods, ICFEM 2011, Durham,
               UK, October 26-28, 2011. Proceedings},
  booktitle = {ICFEM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6991},
  year      = {2011},
  isbn      = {978-3-642-24558-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-24559-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Spivey96,
  author    = {John Michael Spivey},
  title     = {The Z notation - a reference manual},
  publisher = {Prentice Hall},
  series    = {Prentice Hall International Series in Computer Science},
  year      = {1989},
  isbn      = {978-0-13-983768-5},
  pages     = {I-XI, 1-155},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{Dasgupta2006,
author = {Sanjoy Dasgupta,Christos Papadimitriou,Umesh Vazirani},
title = {Algorithms},
publisher = {Mc Graw Hill},
year = {2006}
}

@Article{Leibnizens,
author = {By Karl Immanuel
Gerhardt, Gottfried
Wilhelm Leibniz},
title = {Leibnizens mathematische Schriften},
journal = {G. H. Pertz},
year = {1859},
note = "Available at: http://www.archive.org/details/leibnizensmathe07leibgoog.  Accessed on  January 10, 2012."

}


@Unpublished{Daniel2004,
author = {Daniel S. Wilkerson},
title = {Why the '+1' in Two's Complement Arithmetic?},
note = "Available at http://daniel-wilkerson.appspot.com/twos_complement.html",
OPTkey = {•},
year = {2004},
month = {June}

}


@Book{Mano1979,
author = {M. Morris Mano},
editor = {Prentice-Hall},
title = {Digital logic and computer design  },
publisher = {Prentice-Hall College},
year = {1979}
}



@Book{James2010,
author = {James L. Hein, Emeritus},
title = {Discrete Structures, Logic, and Computability},
publisher = {Portland State University},
year = {2010}
}

% This file was created with JabRef 2.6.
% Encoding: MacRoman

@INPROCEEDINGS{Rodin,
  author = {Jean-Raymond Abrial},
  title = {A System Development Process with Event-B and the Rodin Platform},
  booktitle = {Formal Methods and Software Engineering},
  year = {2007},
  pages = {1-3},
  address = {Berlin},
  organization = {ICFEM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/icfem/2007},
  ee = {http://dx.doi.org/10.1007/978-3-540-76650-6_1}
}

@inproceedings{BHDL_2003,
  author    = {Ammar Aljer and
               Philippe Devienne and
               Sophie Tison and
               Jean-Louis Boulanger and
               Georges Mariano},
  title     = {BHDL: Circuit Design in B},
  booktitle = {ACSD},
  year      = {2003},
  pages     = {241-242},
  ee        = {http://csdl.computer.org/comp/proceedings/acsd/2003/1887/00/18870241.pdf},
  crossref  = {DBLP:conf/acsd/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/acsd/2003,
  title     = {3rd International Conference on Application of Concurrency
               to System Design (ACSD 2003), 18-20 June 2003, Guimaraes,
               Portugal},
  booktitle = {ACSD},
  publisher = {IEEE Computer Society},
  year      = {2003},
  isbn      = {0-7695-1887-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{DBLP:conf/birthday/ChrzaszczW07,
  author = {Jacek Chrzaszcz and Daria Walukiewicz-Chrzaszcz},
  title = {Towards Rewriting in Coq},
  booktitle = {Rewriting, Computation and Proof},
  year = {2007},
  pages = {113-131},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/birthday/2007jouannaud},
  ee = {http://dx.doi.org/10.1007/978-3-540-73147-4_6}
}

@INPROCEEDINGS{DBLP:conf/eurovav/Dondossola99,
  author = {Giovanna Dondossola},
  title = {Formal Methods for the Engineering and Certification of Safety-critical
	Knowledge-based Systems},
  booktitle = {EUROVAV},
  year = {1999},
  pages = {113-129},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/eurovav/1999}
}

@TECHREPORT{ClearsyMathRule,
  author = {Thierry Lecomte},
  title = {Writing Mathematical Rules},
  institution = {Clearsy},
  year = {2008},
  crossref = {Mathematical_Rule_Clearsy},
  keywords = {The Mathematical Rule Language},
  timestamp = {2010.10.04},
  url = {http://www.tools.clearsy.com/index.php5?title=Writing_Mathematical_Rules_1.1}
}

@INPROCEEDINGS{DBLP:conf/fmco/Leuschel08,
  author = {Michael Leuschel},
  title = {Towards Demonstrably Correct Compilation of Java Byte Code},
  booktitle = {FMCO},
  year = {2008},
  pages = {119-138},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/fmco/2008},
  ee = {http://dx.doi.org/10.1007/978-3-642-04167-9_7}
}

@INPROCEEDINGS{DBLP:conf/mpc/Morgan89,
  author = {Carroll Morgan},
  title = {Types and Invariants in the Refinement Calculus},
  booktitle = {MPC},
  year = {1989},
  pages = {363-378},
  address = {Amsterdam},
  organization = {Science of Computer Programming},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/mpc/1989}
}

@INPROCEEDINGS{DBLP:conf/tapsoft/B-Core95,
  title = {B-Core: The B-Toolkit Demonstration},
  booktitle = {TAPSOFT},
  year = {1995},
  pages = {805-806},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tapsoft/1995},
  ee = {http://dx.doi.org/10.1007/3-540-59293-8_243}
}

@BOOK{Abrial,
  title = {The B Book: Assigning Programs to Meanings.},
  publisher = {Cambridge University Press},
  year = {1996},
  author = {J. R. Abrial },
  edition = {1},
  alteditor = {Cambridge University Press},
  key = {0}
}

@MISC{abrial:03,
  author = {J.-R. Abrial and D. Cansell},
  title = {Click'n'Prove - Interactive Proofs Within Set Theory. Version 23.},
  month = {Mai},
  year = {2003},
  note = {Available at: http://www.loria.fr/\~{}cansell/rome.ps.gz. Accessed  
	in may 2007}
}

@INPROCEEDINGS{ALBSG:MICRO36,
  author = {Vikram Adve and Chris Lattner and Michael Brukman and Anand Shukla
	and Brian Gaeke},
  title = {{LLVA: A Low-level Virtual Instruction Set Architecture}},
  booktitle = {{Proceedings of the 36th annual ACM/IEEE international symposium
	on Microarchitecture (MICRO-36)}},
  year = {2003},
  address = {San Diego, California},
  month = {Dec}
}


@MISC{bcore,
  author = {B-Core},
  title = {A Comparison of {Z} and VDM with {B}/{A}{M}{N}},
  month = {agos},
  year = {1999},
  note = {Available at: http://www.b-core.com/ZVdmB.html. Accessed on 18 April
	2007},
  key = {0}
}

@INPROCEEDINGS{DBLP:conf/tapsoft/B-Core95,
  author = {B-Core},
  title = {TAPSOFT'95: Theory and Practice of Software Development, 6th International
	Joint Conference CAAP/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings},
  booktitle = {TAPSOFT},
  year = {1995},
  pages = {805-806},
  address = {Berlin},
  organization = {ICFTAPSOFT'95EM},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{DBLP:conf/fm/BlazyDL06,
  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
  title = {Formal Verification of a C Compiler Front-End},
  booktitle = {FM},
  year = {2006},
  pages = {460-475},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/11813040_31}
}

@INPROCEEDINGS{Brukadt,
  author = {Randy Burkhardt},
  title = {An {I}{S}{O} Standard Guards the {A}da {H}en {H}ouse},
  booktitle = {ADA},
  year = {2000},
  address = {United States of America},
  month = {Janeiro},
  organization = {IEEE},
  note = {Available at: http://ieeexplore.ieee.org/xplore/login.jsp?url=/iel5/52/17783/00820017.pdf
	Accessed on 18 April 2007},
  key = {2}
}

@MISC{CANSELL,
  author = {D. M\'ARY CANSELL},
  title = { Foundations of the {B} Method},
  month = {abril},
  year = {2003},
  note = {Available at: {$<$http://www2.imm.dtu.dk/~db/cai/cai-b.pdf$>$}. Accessed on 18 April 2007},
  key = {0}
}

@MISC{atelierB,
  author = {Clearsy},
  title = {Atelier {B} web site},
  howpublished = {Available at: {http://www.atelierb.eu}},
  year = {2009},
  note = { Accessed on January 10, 2012.}
}

@MISC{ComenC,
  author = {ClearSy},
  title = {ComenC, B0 Implementation Translation into C Language},
  howpublished = {Available at:http://www.comenc.eu },
  year = {2008},
  institution = {ClearSy System Engineering }
}

@TECHREPORT{CLEARSY,
  author = {Clearsy},
  title = {Atelier B},
  institution = {Clearsy},
  year = {2005},
  address = {http://www.atelierb.eu},
  date-added = {2010-04-19 20:18:32 -0300},
  date-modified = {2010-04-19 20:20:36 -0300}
}

@MANUAL{B_reference,
  title = {B Language Reference Manual},
  author = {Clearsy},
  organization = {Clearsy System Engineering},
  address = {Fran\c{c}a},
  edition = {1},
  month = {Janeiro},
  year = {2004},
  note = {Available at:http://www.b4free.com/paper\_links.htm. Acessed 18 April 2007},
  key = {0},
  version = {1.8.5}
}

@MISC{Javacc,
  author = {CollabNet},
  title = {{J}ava{C}{C} Home},
  howpublished = {Available at: https://javacc.dev.java.net },
  year = {2007},
  institution = {CollabNet }
}

@MISC{Cury,
  author = {Edson Cury},
  title = {Certifica\c{c}\~ao de Software},
  howpublished = {Available at:http://www.aviacao\-civil.ifi.cta.br/Cursos/SeminarioRCF\_2003},
  year = {2007},
  note = {Accessed on 14 May 2007},
  key = {3}
}

@INPROCEEDINGS{deharbe06developing,
  author = {David D\'{e}harbe and Bruno Gurgel Gomes and Anamaria Martins Moreira},
  title = {{A}utomation of {J}ava {C}ard {C}omponent {D}evelopment using the
	{B} {M}ethod},
  booktitle = {11th IEEE International Conference on Engineering of Complex Computer
	Systems (ICECCS'06)},
  year = {2006},
  pages = {259--268},
  address = {Los Alamitos, CA, USA},
  publisher = {IEEE Computer Society}
}

@INPROCEEDINGS{Valerio_SBMF09,
  author = {V. G. Medeiros{\ }Jr. and David D\'{e}harbe},
  title = {Formal {C}onstruction of a {M}icrocontroller {I}nstruction {S}et {M}odel {U}sing {B}},
  booktitle = {Brazilian Symposium on Formal Methods},
  year = {2009},
  address = { Gramado - RS},
  organization = {SBMF}
}

@INPROCEEDINGS{Dantas_SBMF08,
  author = {B. P. Dantas and David D\'{e}harbe and S. L. Galvão and A. M.
	Moreira and V. G. Medeiros{\ }Jr.},
  title = {Applying the {B} method to take on the grand challenge of verified
	compilation},
  booktitle = {Brazilian Symposium on Formal Methods},
  year = {2008},
  address = { Salvador - BA},
  organization = {SBMF}
}

@INPROCEEDINGS{DantasSemish2008,
  author = {B. P. Dantas and D. D\'{e}harbe and S.S.L. Galvão and A. Martins and V. G. Medeiros},
  title = {Proposta e Avalia\c{c}ão de uma Abordagem de Desenvolvimento de Software
	Fidedigno por Constru\c{c}ão com o M\'{e}todo {B}},
  booktitle = {Semin\'ario Integrado de Software e Hardware},
  year = {2008},
  address = { Bel\'{e}m - PA},
  organization = {XXXV SEMISH},
  ee = {http://www.lbd.dcc.ufmg.br:8080/colecoes/semish/2008/014.pdf}
}

@ARTICLE{DBLP:journals/entcs/EvansG08,
  author = {Neil Evans and Neil Grant},
  title = {Towards the Formal Verification of a Java Processor in Event-B},
  journal = {Electronic Notes in Theoretical Computer Science.},
  year = {2008},
  volume = {201},
  pages = {45-67},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1016/j.entcs.2008.02.015}
}





@MISC{Fabian2008,
  author = {Fabian Fritz},
  title = {An Object Oriented Parser For B Specifications},
  year = {2008},
  address = {Available at:http://www.formal-methods.de/thesis/Fritz2008-Bachelorarbeit.pdf.pdf.
	},
  institution = {Institut for Informatik Softwaretechnik und Programmiersprachen},
  school = {Heinrich Heine}
}

@ARTICLE{DBLP:journals/dt/GajskiV95,
  author = {Daniel D. Gajski and Frank Vahid},
  title = {Specification and Design of Embedded Hardware-Software Systems},
  journal = {IEEE Design {\&} Test of Computers},
  year = {1995},
  volume = {12},
  pages = {53-67},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.ieeecomputersociety.org/10.1109/54.350695}
}

@MISC{gcc,
  author = {Gcc Developer Community - GNU},
  title = {GCC, the GNU Compiler Collection},
  howpublished = {Available at: http://gcc.gnu.org },
  year = {1999},
  institution = { GNU }
}

@ARTICLE{Hartel2001,
  author = {Hartel,, Pieter H. and Moreau,, Luc},
  title = {{F}ormalizing the safety of {J}ava, the {J}ava virtual machine, and
	{J}ava card},
  journal = {ACM Comput. Surv.},
  year = {2001},
  volume = {33},
  pages = {517--558},
  number = {4},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/503112.503115},
  issn = {0360-0300},
  publisher = {ACM}
}

@INPROCEEDINGS{HOARE,
  author = {C. A. R. Hoare},
  title = {The verifying compiler, a grand challenge for computing research},
  booktitle = {VMCAI},
  year = {2005},
  pages = {78-78},
  date-added = {2010-04-19 20:26:20 -0300},
  date-modified = {2010-04-19 20:27:34 -0300}
}

@PROCEEDINGS{Tony_Hoare,
  title = {The Verifying Compiler: A GrandChallenge for Computing Research},
  year = {2005},
  address = {UK},
  publisher = {Workshop on Grand Challenges for Computing Research},
  note = {Available at:http://www.nesc.ac.uk/esi/events/Grand\_Challenges/workshop02.html
	Accessed on 18 April 2007},
  month = {Jan},
  organization = {UK Computing Research Committee},
  author = {Tony Hoare},
  institution = {Microsoft Research Ltd.}
}

@BOOK{IOVINE,
  title = {PIC Microcontroller Project Book},
  publisher = {McGraw-Hill},
  year = {2000},
  editor = {McGraw-Hill},
  author = {John IOVINE},
  volume = {1},
  address = {New York},
  note = {203p.},
  key = {0}
}

@TECHREPORT{GEMPLUS_99,
  author = {L. Casset; J. L. Lanet},
  title = {A Formal Specification of the Java Bytecode Semantics using the {B}
	method},
  institution = {Gemplus},
  year = {1999},
  date-added = {2010-04-19 19:17:53 -0300},
  date-modified = {2010-04-19 20:18:30 -0300}
}

@BOOK{LAM,
  title = {Hardware Design Verification: Simulation and Formal Method-Based
	Approaches},
  publisher = {Prentice Hall PTR},
  year = {2003},
  editor = {Prentice Hall},
  author = {William K LAM},
  volume = {1},
  address = {New York},
  note = {624p.},
  key = {0}
}

@INPROCEEDINGS{DBLP:conf/sefm/LeinenbachPP05,
  author = {Dirk Leinenbach and Wolfgang J. Paul and Elena Petrova},
  title = {Towards the Formal Verification of a C0 Compiler: Code Generation
	and Implementation Correctnes},
  booktitle = {SEFM},
  year = {2005},
  pages = {2-12},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.51}
}

@INPROCEEDINGS{DBLP:conf/popl/Leroy06,
  author = {Xavier Leroy},
  title = {Formal certification of a compiler back-end or: programming a compiler
	with a proof assistant},
  booktitle = {POPL},
  year = {2006},
  pages = {42-54},
  address = {France},
  organization = {INRIA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/1111037.1111042}
}

@ARTICLE{xavier,
  author = {Xavier Leroy},
  title = {Formal Certification of a Compiler Back-end},
  journal = {INRIA Rocquencourt},
  year = {2006},
  note = {Available at:http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf
	Accessed on 14 May 2007}
}

@INPROCEEDINGS{proB,
  author = {Michael Leuschel and Michael Butler},
  title = {Pro{B}: {A} Model Checker for {B}},
  booktitle = {FME 2003: Formal Methods},
  year = {2003},
  editor = {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
  series = {LNCS 2805},
  pages = {855--874},
  address = {Pisa, Italy},
  publisher = {Springer},
  isbn = {3-540-40828-2}
}

@MASTERSTHESIS{LAUT_LIMA,
  author = {Carlos Eduardo Guimarães Lima},
  title = {Automa\c{c}ão de Testes de Produ\c{c}ão e Determina\c{c}ão de BS\&W de po\c{c}os
	produtores de petr\'oleo},
  school = {UFRN},
  year = {2000},
  address = {Natal},
  institution = {Programa de P\'os-Gradua\c{c}ão em Engenharia El\'{e}trica, Universidade Federal
	do Rio Grande do Norte}
}

@MISC{maquina_turing,
  author = {A Encicliop\'{e}dia Livre},
  title = {M\'aquinas de Turing},
  howpublished = {on-line},
  year = {2006},
  note = {Available at:http://pt.wikipedia.org/wiki/M\'aquina\_de\_Turing. Accessed on 18 April 2007},
  key = {10}
}

@TECHREPORT{GEMPLUS_99,
  author = {Casset Ludovic and Jean Louis Lanet},
  title = {{A} {F}ormal {S}pecification of the {J}ava {B}ytecode {S}emantics
	using the {B} method},
  institution = {Gemplus},
  year = {1999},
  address = {France},
  organization = {.}
}

@INPROCEEDINGS{Batcave,
  author = {Eberton S. Marinho and Val\'{e}rio G. Medeiros Jr and David B. P. D\'{e}harbe
	and Bruno Gomes and Cl\'audia Tavares },
  title = {{A} {F}erramenta {B}atcave para a {V}erifica\c{c}ão de {E}specifica\c{c}\~oes
	{F}ormais na {N}ota\c{c}ão {B}},
  booktitle = {Sessão de Ferramentas},
  year = {2008},
  address = {Campinas, SP},
  organization = {Simp\'osio Brasileiro de Engenharia de Software (SBES)}
}

@MISC{MedeirosJr2007,
  author = {Val\'{e}rio Gutemberg de Medeiros},
  title = {Aplica\c{c}ão do m\'{e}todo B para a constru\c{c}ão de programas assembly},
  howpublished = {Relat\'orio de gradua\c{c}ão - Dimap},
  year = {2007},
  note = {Natal/RN}
}



@INPROCEEDINGS{Ermac2008,
  author = {Val\'{e}rio G. Jr Medeiros and Stephenson S. L. Galvão and David D\'{e}harbe},
  title = {{M}odelagem de Microcontroladores em {B}},
  booktitle = {Anais do VIII ERMAC},
  year = {2008},
  address = { Natal - RN},
  organization = {Encontro Regional de Matem\'atica Aplicada e Computacional}
}

@TECHREPORT{relat_PIC16,
  author = {Microchip},
  title = { PIC16C432 - Data Sheet OTP 8-Bit CMOS MCU with LIN Transceiver},
  institution = {Microchip Technology Inc},
  year = {2002},
  address = {USA},
  note = {197p.},
  key = {DS41140B}
}

@MISC{anamaria,
  author = {Anamaria Martis Moreira and David D\'{e}harbe},
  title = {Tutorial: Software Engineering with the {B} method},
  howpublished = {Tutorial - SBMF},
  year = {2005},
  note = {Available at:http://www.dimap.ufrn.br/~anamaria/Files/BtutorialSBMF2005.pdf.
	Accessed 18 April 2007}
}

@ARTICLE{Palsberg:92,
  author = {Jens Palsberg},
  title = {A Provably Correct Compiler Generator},
  journal = {Dinamarca},
  year = {1992},
  note = {Available at:http://www.cs.ucla.edu/\~palsberg/paper/esop92.pdf.
	Accessed on 22 de July 2007},
  optkey = {0},
  optpages = {38}
}

@BOOK{PRESSMAN,
  title = {Engenharia de Software},
  publisher = {Makron Books},
  year = {1995},
  editor = {São Paulo},
  author = {Roger S. PRESSMAN},
  volume = {1},
  address = {São Paulo},
  edition = {6},
  note = {752p.},
  key = {0}
}

@MISC{Ramasamy03formalverification,
  author = {Harigovind V. Ramasamy and Michel Cukier and William H. Sanders},
  title = {Formal Verification of an Intrusion-Tolerant Group Membership Protocol},
  year = {2003}
}

@MISC{robinson:03,
  author = {K. Robinson},
  title = {An Introduction to the {B} Method - An Overview},
  year = {2003},
  note = {Available at: http://www.cse.unsw.edu.au/~cs2110/PDF/overview-notes.pdf.
	Accessed on 14 May 2007}
}

@BOOK{SCHNEIDER,
  title = {The {B}-method an introduction.},
  publisher = {PALGRAVE MACMILLAN},
  year = {2001},
  author = {Steve Schneider },
  volume = {1},
  number = {1},
  series = {1},
  address = {Great Britain},
  edition = {1},
  key = {0}
}

@MASTERSTHESIS{LAUT_SERGIO,
  author = {Paulo S\'{e}rgio Silva},
  title = {Automa\c{c}ão Da Drenagem No Teste De Produ\c{c}ão Convencional
	Em Tanque Cil\'indrico},
  school = {UFRN-PPgEEC},
  year = {2008}
}

@MISC{Simulator_z80,
  author = {Vladimir Soso},
  title = {Z80 Simulator {I}{D}{E}},
  howpublished = {On-line},
  year = {2002},
  note = {Available at: http://www.oshonsoft.com. Accessed on January 10, 2012.}
}

@BOOK{SOUSA,
  title = {Conectando o PIC 16F877A Recursos Avan\c{c}ados},
  publisher = {\'{e}rica},
  year = {2003},
  editor = {São Paulo},
  author = {David SOUSA and Nicolas LAVINIA},
  address = {São Paulo},
  edition = {2},
  note = {380p.},
  key = {0}
}

@MISC{Java,
  author = {Sun},
  title = {Sun Microsystems Home Page},
  howpublished = {Available at: http://www.java.sun.com},
  year = {2009},
  institution = {Sun Microsystems }
}

@INPROCEEDINGS{Velev04,
  author = {Miroslav N. Velev},
  title = {Efficient formal verification of pipelined processors with instruction
	queues},
  booktitle = {ACM Great Lakes Symposium on VLSI},
  year = {2004},
  pages = {92-95},
  ee = {http://doi.acm.org/10.1145/988952.988975}
}

@INPROCEEDINGS{Tatibouet,
  author = {J. C. Voisinet},
  title = {{JB}tools: an experimental platform for the formal {B} method},
  booktitle = {Proceedings of the inaugural conference on the {P}rinciples and {P}ractice
	of {P}rogramming in {J}ava (PPPJ'02 )},
  year = {2002},
  pages = {137--139},
  address = {Dublin, Ireland},
  publisher = {National University of Ireland}
}

@BOOK{J.B,
  title = {Software Engineering with B},
  publisher = {Addison-Wesley},
  year = {1996},
  editor = {England},
  author = {J.B Wordsworth },
  address = {England},
  note = {331p.},
  key = {0}
}



@inproceedings{DBLP:conf/asm/Wright08,
  author    = {Stephen Wright},
  title     = {Using Event {B} to Create a Virtual Machine Instruction Set
               Architecture},
  booktitle = {ABZ},
  year      = {2008},
  pages     = {265-279},
  ee        = {http://dx.doi.org/10.1007/978-3-540-87603-8_21},
  crossref  = {DBLP:conf/asm/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/asm/2008,
  editor    = {Egon B{\"o}rger and
               Michael J. Butler and
               Jonathan P. Bowen and
               Paul Boca},
  title     = {Abstract State Machines, B and Z, First International Conference,
               ABZ 2008, London, UK, September 16-18, 2008. Proceedings},
  booktitle = {ABZ},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5238},
  year      = {2008},
  isbn      = {978-3-540-87602-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}




@MANUAL{UndocumentedZ80,
  title = {The Undocumented Z80 Documented},
  author = { Sean Young },
  month = {November},
  year = {2003},
  note = {Available at: http://www.myquest.nl/z80undocumented/z80-documented.pdf.
	Accessed on January 10, 2012.},
  version = {0.6}
}

@BOOK{Coq_Book,
  title = {Interactive Theorem Proving and Program Development: {C}oq'Art: the
	Calculus of Inductive Constructions .},
  publisher = {Springer},
  year = {2004},
  author = {Yves Bertot, Pierre Castran},
  volume = {1},
  number = {1},
  series = {1},
  edition = {1},
  key = {0}
}

@MANUAL{Z80_manual,
  title = {Z80 Family CPU User Manual},
  author = {Zilog},
  organization = {ZiLOG Worldwide Headquarters},
  address = {910 E. Hamilton Avenue},
  year = {2001},
  note = {Available at:http://www.zilog.com/docs/z80/um0080.pdf. Accessed on January 10, 2012.}
}

@PROCEEDINGS{DBLP:conf/fmco/2008,
  title = {Formal Methods for Components and Objects, 7th International Symposium,
	FMCO 2008, Sophia Antipolis, France, October 21-23, 2008, Revised
	Lectures},
  year = {2009},
  editor = {Frank S. de Boer and Marcello M. Bonsangue and Eric Madelain},
  volume = {5751},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FMCO},
  ee = {http://dx.doi.org/10.1007/978-3-642-04167-9},
  isbn = {978-3-642-04166-2}
}

@PROCEEDINGS{DBLP:conf/icfem/2007,
  title = {Formal Methods and Software Engineering, 9th International Conference
	on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November
	14-15, 2007, Proceedings},
  year = {2007},
  editor = {Michael Butler and Michael G. Hinchey and Mar\'{\i}a M. Larrondo-Petrie},
  volume = {4789},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {ICFEM},
  isbn = {978-3-540-76648-3}
}

@PROCEEDINGS{DBLP:conf/birthday/2007jouannaud,
  title = {Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre
	Jouannaud on the Occasion of His 60th Birthday},
  year = {2007},
  editor = {Hubert Comon-Lundh and Claude Kirchner and H{\'{e}}l{\`e}ne Kirchner},
  volume = {4600},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {Rewriting, Computation and Proof},
  isbn = {978-3-540-73146-7}
}

@PROCEEDINGS{DBLP:conf/tapsoft/1995,
  title = {TAPSOFT'95: Theory and Practice of Software Development, 6th International
	Joint Conference CAAP/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings},
  year = {1995},
  editor = {Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach},
  volume = {915},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TAPSOFT},
  isbn = {3-540-59293-8}
}

@PROCEEDINGS{DBLP:conf/tapsoft/1995,
  title = {TAPSOFT'95: Theory and Practice of Software Development, 6th International
	Joint Conference CAAP/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings},
  year = {1995},
  editor = {Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach},
  volume = {915},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TAPSOFT},
  isbn = {3-540-59293-8}
}

@PROCEEDINGS{DBLP:conf/mpc/1989,
  title = {Mathematics of Program Construction, 375th Anniversary of the Groningen
	University, International Conference, Groningen, The Netherlands,
	June 26-30, 1989, Proceedings},
  year = {1989},
  editor = {Jan L. A. van de Snepscheut},
  volume = {375},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {MPC},
  isbn = {3-540-51305-1}
}

@PROCEEDINGS{DBLP:conf/eurovav/1999,
  title = {Validation and Verification of Knowledge Based Systems - Theory,
	Tools and Practice, Collected papers from EUROVAV '99, 5th European
	Symposium on Validation and Verification of Knowledge Based Systems,June
	9-11, 199, Oslo, Norway},
  year = {1999},
  editor = {Anca I. Vermesan and Frans Coenen},
  publisher = {Kluwer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {EUROVAV},
  isbn = {0-7923-8645-0}
}

@PROCEEDINGS{DBLP:conf/acsd/2003,
  title = {3rd International Conference on Application of Concurrency to System
	Design (ACSD 2003), 18-20 June 2003, Guimaraes, Portugal},
  year = {2003},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {ACSD},
  isbn = {0-7695-1887-7}
}

